T:Type, E, E':(TT).
(x, y:T. E(x,y)  E'(x,y))  ((x,y:T. E(x,y)) <>{T} (x,y:T. E'(x,y))) 

latex

Up	gen algebra 1
Definitions of Statement	E <>{T} E', x,y:T. E(x;y)
Definitions	t  T, x,y:T. E(x;y), E <>{T} E', x(s1,s2), P  Q, , x:A. B(x)
Lemmas	iff wf